FDL - Nuprl Definition : l_succ

Nuprl Definition : l_succ

y = succ(x) in l

P(y) ==

i:

. i+1<||l||

l[i] = x

P(l[i+1])

clarification:

y

T = succ(x) in l

P(y) ==

i:

. i+1<||l||

l[i] = x

T

P(l[i+1])

Definitions x:A. B(x), , ||as||, P Q, l[i]

FDL editor aliases l_succ